\begin{tabbing}
w{-}es\=\{i:l\}\+
\\[0ex](${\it the\_w}$; $p$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$<$w{-}E(${\it the\_w}$)\+
\\[0ex], product{-}deq(Id;$\mathbb{N}$;IdDeq;NatDeq)
\\[0ex], $\lambda$$e$.w{-}pred(${\it the\_w}$;$e$)
\\[0ex], $\lambda$$e$.w{-}info(${\it the\_w}$;$e$)
\\[0ex], TERMOF\{w{-}order{-}axioms:ObjectId, 1:l, i:l\}(${\it the\_w}$,$p$)
\\[0ex], ${\it the\_w}$.T
\\[0ex], ${\it the\_w}$.TA
\\[0ex], ${\it the\_w}$.M
\\[0ex], $\lambda$$i$,$x$. w{-}s(${\it the\_w}$; $i$; 0; $x$)
\\[0ex], $\lambda$$i$.(w{-}machine(${\it the\_w}$;$i$).2).1
\\[0ex], $\lambda$$e$.w{-}eval(${\it the\_w}$; $e$)
\\[0ex], $\lambda$$i$.w{-}machine(${\it the\_w}$;$i$).2.2
\\[0ex], $\lambda$$i$.w{-}machine(${\it the\_w}$;$i$).1
\\[0ex], $\lambda$$e$.w{-}time(${\it the\_w}$; $e$)
\\[0ex], TERMOF\{world{-}es{-}val:ObjectId, 1:l, i:l\}(${\it the\_w}$,$p$)
\\[0ex], TERMOF\{w{-}causl{-}time2:ObjectId, 1:l, i:l\}(${\it the\_w}$,$p$)
\\[0ex], $\lambda$$i$,$x$. w{-}discrete(${\it the\_w}$;$i$;$x$)
\\[0ex], TERMOF\{world{-}es{-}const:ObjectId, 1:l, i:l\}(${\it the\_w}$,$p$)
\\[0ex], $\cdot>$
\-
\end{tabbing}